k:Knd, x:Id, n:Top, f:(VoidVoidTop). update-spec1(k;x;n;s,v.f(s,v))  kz:KndId fp Top 

latex

Definitions	Knd, t  T, Id, Top, Void, Type, x:AB(x), x:A. B(x), car.cdr, x.A(x), <a,b>, nil, x:AB(x), x:A. B(x), x. t(x), x : v, update-spec1(k;x;n;s,v.f(s;v))
Lemmas	fpf-single wf, top wf, Id wf, Knd wf